x:(), r:, k:, y:( List).
(k  ||y||)
 0 < x(k)
 (q-rel(r;q-linear(k;j.x(j);y))
  q-rel(r;y[(k - 1)] + ((1/x(k)) * q-linear(k - 1;j.x(j);y)))) 

latex

Definitions

ff, tt, if b then t else f fi , q-rel(r;x), P & Q, False, x. t(x), t  T, True, T, , P  Q, A, P  Q, A  B, P  Q, , x:A. B(x), Unit, , x(s), , , S  T

Lemmas

qmul-qdiv-cancel3, qadd comm q, qmul one qrng, qmul-qdiv-cancel4, qmul zero qrng, qmul over plus qrng, not functionality wrt iff, assert of bnot, eqff to assert, assert of eq int, eqtt to assert, iff transitivity, qmul preserves qless, qle wf, qmul preserves qle, not wf, bnot wf, assert wf, bool wf, eq int wf, qinv-positive, qless irreflexivity, qle weakening eq qorder, qless transitivity 2 qorder, nat plus wf, length wf1, nat plus inc, qless wf, le wf, q-linear wf, int inc rationals, qdiv wf, qmul wf, select wf, qadd wf, nat wf, q-linear-unroll, rationals wf, q-rel wf, true wf, squash wf, iff wf